Description of Terms
First, terms appearing in the specification will be defined.
(1) Protocol: protocol means communication rules between modules in a system in which a plurality of modules (various communication devices such as exchanges, terminals, or local function units in the system) achieve a predetermined object as a whole by transmitting and receiving signals. PA0 (2) Process: process means a module which is a communication entity in the protocol. PA0 (3) Channel: channel means a signal transmission line having a directivity present between processes, and transmission and reception of signals are necessarily made through a channel from the transmission process to a reception process. PA0 (4) Transmission and reception: transmission means that a process puts a signal in a channel to a destination process, reception means that a process takes out a signal from the top of a channel from a transmission process, and taking out of the signal from the channel is performed in the order of putting into the channel. There is no time limitation to the reception of the transmitted signal and, therefore, a once transmitted signal is eventually received. PA0 (5) Process state: process state means a state taken by a process when it operates, including various states such as READY or IDLE, WAIT, REGISTER, SERVICE and FAULT, and the process transits its state every time the process transmits or receives a signal. Initial state can be flexibly set. PA0 (6) Send-transition and receive-transition: send-transition means a transition of process state associated with transmission, and receive-transition means a transition of process state associated with reception. PA0 (7) Protocol specification: protocol specification describes behaviors to be taken by individual processes in a system. PA0 (8) Channel state: channel state shows what and how many signals are put in a channel in what order, and when the number of signals is zero, the channel is referred to as empty. PA0 (9) System state: system state is defined as a set of individual process states and individual channel states in the entire system, when transmission or reception is performed, the process state and the channel state are changed, and the system state transits. PA0 (10) Initial system state: initial system state means a system state where all processes are in the initial states and all channels are empty. PA0 (11) Stable state: stable state means a system state where all channels are empty. PA0 (12) Reachable system state: reachable system state means a system state which can be reached by executing executable state transitions from the initial system state, and also means the initial system state itself. PA0 (13) Reachable process state: reachable process state means a process state constituting a reachable system state. PA0 (14) Executable state transition: executable state transition includes an executable send-transition and an executable receive-transition. Executable send-transition means a send-transition from a reachable process state. Executable receive-transition means a receive-transition from a reachable process state, where the reception signal is at the top of channel in a reachable system state including the reachable process state. PA0 (15) Protocol error: protocol specification can be described regardless of the reachability of a system state or the executability of a process state transition. Therefore, the protocol may include a logical contradiction, and a logical contradiction included in the protocol specification is referred to as protocol error. Protocol error includes a deadlock and one which relates to behavior of each process. PA0 (16) Deadlock: deadlock means a system condition which cannot transit any further, since any of processes constituting the system state have no executable state transition. PA0 (17) Protocol error related to operation of each process: this protocol error includes an unexecutable transition, overflow, undefined reception, and the like. The unexecutable transition means a state transition which is defined in the protocol specification but is not executable. Overflow means a state where a process transmits signals beyond a predetermined channel capacity. Undefined reception means a receive-transition which is executable but is not defined in the protocol specification. PA0 (1) First, an initial node indicating the initial state is generated for each process, and an initial state of each of the other processes is set as a least state of each of other processes for the initial node of each process. For example, for process 2, when an initial node indicating the initial state IDLE. 0 is generated in FIG. 9(b), the initial state READY. 0 of process 1 is set to the initial node of process 2 as the least state of process 1 for the initial state IDLE. 0 of process 2. PA0 (2) Then, addition of an executable send-transition and addition of an executable receive-transition are repeated to generate a state transition graph of each process and, at the same time, all stable states (system state where all channels are empty) are enumerated to detect deadlocks. PA0 (3) The procedure for enumeration of stable states will now be described. First, since the initial system state (e.g. READY 0, IDLE 0) where all processes are in initial states is a stable state, when the initial node of each process is generated to generate the state transition graph of each process, this stable state is generated and stored in the memory as an element of a stable state set. Then, in generating the state transition graph of each process, every time a node is generated by addition of a new receive-transition, an original stable state is found among the existing stable state set, the state before signal transmission in the found stable state is replaced with the state after signal transmission, and the state before signal reception is replaced with the state after signal reception to generate a new stable state. Further, the new stable state is stored in the memory to add it to the stable state set. For example, in FIG. 9(b), when a node representing the state SERVICE. 0 is generated by addition of the receive-transition +REQ of process 2, the original stable state (READY. 0, IDLE. 0) is found among the stable state set, the state READY. 0 of process 1 is replaced with the state WAIT. 0 after execution of the send-transition -REQ, and the state IDLE. 0 of process 2 is replaced with tho state SERVICE. 0 after execution of the receive-transition REQ to generate a new stable state (WAIT. 0, SERVICE. 0), which is then added to the stable state set. PA0 (4) On the other hand, in generating the state transition graph of each process, every time a new node is generated by addition of a new executable state transition, the least state of each of other processes for the state represented by that node is set to the node. For example, for process 2, when a node representing the state SERVICE. 0 is generated by addition of the receive-transition of signal REQ to the initial node in FIG. 9(b), the least state WAIT. 0 of process 1 for the state SERVICE. 0 is set. PA0 (5) A protocol error related to behavior of the process is detected by generating the state transition graph of each process as shown above. That is, in the generation of a state transition graph of a process, when the receive-transition of executable state transition is added, a check is made as to whether or not the receive-transition is defined in the protocol specification. If undefined, it is determined as undefined reception. Further, when the send-transition of executable state transition is added, the number of signals in the channel when other processes reach the least states for the state represented by the node of the transition destination is checked. If it exceeds a predetermined channel capacity, it is determined as overflow. Further, after the completion of generation of all state transition graphs, a check is made as to whether or not there is a state transition which is defined in the protocol specification but has never been added to the state transition graph. If such a transition is found, it is determined as unexecutable transition. For example, in the protocol specification of FIG. 2(b), the receive-transition returning from the state SERVICE of process 2 to the same state SERVICE by reception of the signal ACK is detected as an unexecutable transition, since it has never been added to the state transition graph of process 2 in FIG. 9(b). PA0 (6) On the other hand, after the completion of generation of the state transition graph of each process, if, among the stable state set generated up to the moment, a stable state in which no process state that has send-transition is found, it is detected as a deadlock. In the example shown in FIG. 9, the stable state (WAIT. 2, FAULT. 2) is detected as a deadlock. PA0 (1) a first processing step wherein a state transition graph of each process comprising only executable state transitions of each process is generated according to the transition information of the input protocol specification and, simultaneously, protocol errors related to behavior of each process is detected; and PA0 (2) a second processing step wherein reachable system states among system states defined by combinations of individual process states and individual channel states are successively generated according to the transition information of the generated state transition graph of each process and, among the generated reachable system states, a system state which cannot further transit is detected as deadlock. PA0 (1) in the first processing step, in the generation of the state transition graph of each process, a received state which is a state to which the receiving process transits by receiving a signal for each send-transition is determined, and information thereof is held; and PA0 (2) in the second processing step, in the generation of the reachable system state, using the information of the received state held in the first processing step, a system state after receiving the signal is generated from the system state where the signal still exists in a channel. PA0 (1) in the second processing step, in the generation of the reachable system states, when a next system state is generated from a system state including a plurality of unreceived signals in a channel, the last transmitted signal is selected from the plurality of unreceived signals, and the system state after reception of the selected signal is generated as a next system state. PA0 (1) in the second processing step, in the generation of the reachable system states, when a next system state is generated by executing a send-transition of a process from a system state where the channel is empty, and one or more send-transitions successively exist following the send-transition, the process is advanced to a state of a destination reached by executing the first send-transition and successive send-transitions to produce a next system state. PA0 (1) in the second processing step, in the generation of the reachable system state, when a next system state is generated from a system state including an unreceived signal in a channel, and when a process which has to receive the signal has one or more successive send-transitions at the state after the signal is received, the process is advanced to the state after a series of send-transitions following reception of the signal are all executed to generate a next system state. PA0 (1) in the first processing step, in the generation of the state transition graph of each process, every time a node is added, a state that each of other processes should at least have reached for the process to reach the state represented by the node is determined as a least state, and the information thereof is held; and PA0 (2) in the second processing step, in the generation of the reachable system state, when a next system state is generated from a system state including an unreceived signal in a channel, using the least state information held in the first processing step, if the least state of each of other processes for the state of the transition destination of the receiving process is ahead of the state constituting the system state of the generation source, the state of the other process is advanced to the least state to generate a next system state. PA0 (1) in the first processing step, in the generation of the state transition graph of each process, when two states in a process are equivalent in the sense that transition sequences following the individual states are identical, generation of the state transition graph thereafter and detection of protocol errors are stopped for the later generated state as an equivalence stop state, and information of the equivalence stop state is held; and PA0 (2) in the second processing step, in the generation of the reachable system state, using the information of equivalence stop states held in the first processing step, when an equivalence stop state is included in a system state, generation of system state to be next generated from that system state is stopped. PA0 (1) in the first processing step, in the generation of the state transition graph of each process, when two states in a process are equivalent in the sense that transition sequences following the individual states are identical, generation of the state transition graph thereafter and detection of protocol errors are stopped as an equivalence stop state for the later generated state, and information of the equivalence stop state is held; and PA0 (2) in the second processing step, in the generation of the reachable system state, using the information of the equivalence stop state held in the first processing step, when an equivalence stop state is included in any process between a system state and the system state to be next generated from that system state, generation of the system state to be next generated is stopped. PA0 (1) in the second processing step, in the generation of the reachable system state, when a system state reached by a transition sequence beginning with a send-transition from a system state where all channels are empty and a series of subsequent system states are validated, the send-transition is stored as a validation completion transition, and when the send-transition stored as the validation completion transition appears on the way of generation of system states that follows the transition sequence beginning with another send-transition from the above-mentioned system state where all channels are empty, generation of system state that follows the validation completion transition is stopped. PA0 (A) Whereas in the first conventional method the system state is generated directly from the protocol specification, in the present invention, a system state is generated based on the state transition graph of each process comprising only executable state transitions generated in the first processing step. Therefore, it has an advantage that various additional techniques can be applied to perform more efficient generation of the system state compared with the first conventional method. PA0 (B) Whereas in the first conventional method all of the generated system states have to be stored in a memory, since, in the present invention, every time a system state is generated, a check is made as to whether or not it is able to transit further to detect a deadlock, unnecessary system states are not required to be stored in the memory. (C) Since, in the first conventional method, every time a new system state is generated, all system states must be searched to check whether or not the new system state has already appeared, but the present invention does not require such a time-consuming search processing. PA0 Technique (1) PA0 Technique (2) PA0 Technique (3) PA0 Technique (4) PA0 Technique (5) PA0 Techniques (6) and (7) PA0 Technique (8)